;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ivolume
  (sig volume (ticker data total))
  (sig volume-query (start end tickers tree))
  (con volume-returns-string
       (implies (and (stringp ticker) (natp total))
                (equal t (stringp (volume ticker data total)))))
  (con volume-returns-ticker-natural-pair
       (implies (and (stringp ticker) (natp total))
                (equal t (and (= (len (words (volume ticker data total))) 2)
                              (natp (cadr (words (volume ticker data total))))
                              (> (len (str->chrs (car (words (volume ticker data total))))))))))
  (con volume-query-returns-string
       (implies (and (stringp start) (stringp end))
                (equal t (stringp (volume-query start end tickers tree)))))
  )

